(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const v7 Bool)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const v8 Bool)
(declare-const r6 Real)
(declare-const v9 Bool)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const v10 Bool)
(declare-const r9 Real)
(declare-const v11 Bool)
(declare-const r10 Real)
(declare-const v12 Bool)
(declare-const r11 Real)
(declare-const v13 Bool)
(declare-const r12 Real)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (or (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) v6 (distinct r4 2.0 (- r3) r5)))
(assert (or v6 (distinct r4 2.0 (- r3) r5) v4))
(assert (or v6 v4 (distinct r4 2.0 (- r3) r5)))
(assert (or v4 v6 v4))
(assert (or (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) v4 v6))
(assert (or (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) (distinct r4 2.0 (- r3) r5) (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5))))))
(assert (or v6 v4 v4))
(assert (or v4 v4 v4))
(assert (or (distinct r4 2.0 (- r3) r5) v6 (distinct r4 2.0 (- r3) r5)))
(assert (or v6 v4 v4))
(assert (or (distinct r4 2.0 (- r3) r5) (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5))))))
(assert (or v6 (distinct r4 2.0 (- r3) r5) v6))
(assert (or (distinct r4 2.0 (- r3) r5) v6 v6))
(assert (or v4 (distinct r4 2.0 (- r3) r5) v4))
(assert (or (distinct r4 2.0 (- r3) r5) (distinct r4 2.0 (- r3) r5) (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5))))))
(assert (or (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) (distinct r4 2.0 (- r3) r5) v6))
(assert (or v6 v6 (distinct r4 2.0 (- r3) r5)))
(assert (or (distinct r4 2.0 (- r3) r5) (distinct r4 2.0 (- r3) r5) v6))
(assert (or (distinct r4 2.0 (- r3) r5) (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) (distinct r4 2.0 (- r3) r5)))
(assert (or v6 (distinct (=> v12 v10) v7 (< (* r3 r0 r4) (- r4 r4 r4) r0 98546.0) (< r4 94.4) (distinct (- 98546.0) 12483508.0 (/ r4 (- r4 r4 r4)) r1) (<= r1 95277739373.0 (- (+ 98546.0 r5)))) (distinct r4 2.0 (- r3) r5)))
(check-sat)
